Nuprl Lemma : self_divisor_mul
2,24
postcript
pdf
a
:
,
b
:
.
a
b
|
a
(
b
~ 1)
latex
Definitions
P
Q
,
b
|
a
,
x
:
A
.
B
(
x
)
,
t
T
,
,
a
~
b
,
T
,
True
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
Prop
Lemmas
mul
cancel
in
assoced
,
true
wf
,
squash
wf
,
assoced
wf
,
int
nzero
wf
,
divides
wf
origin
a:
, b:. a
b | a 
(b ~ 1) a:, b:. ab | a (b ~ 1) Qx:A. B(x)
T
T
x:A. B(x)